es:ES, e':E, P:({e:E| loc(e) = loc(e')  Id} ).
(e<e'. P(e))  (((first(e')))  (P(pred(e')) & (e<pred(e'). P(e)))) 

latex

Definitions	t  T, P  Q, x:A. B(x), b, False, A, P & Q, (e <loc e'), loc(e), Id, pred(e), t.1, E, x(s), ES, , first(e), P  Q, P  Q, e<e'. P(e), {T}, P  Q, True, T
Lemmas	squash wf, true wf, es-locl-iff, es-pred-locl, not wf, assert wf, es-first wf, es-locl wf, es-E wf, event system wf, es-pred wf, Id wf, es-loc wf, es-loc-pred